;;;============================================================
;;;
;;; Subject: Equivalence between cmp-d-ls and 
;;;          1dlop-dgop
;;;         
;;;
;;;------------------------------------------------------------
;;;
;;;
;;;============================================================


(in-package "ACL2")


;;;------------------------------------------------------------
;;;
;;; EAT representation
;;;
;;;------------------------------------------------------------

(include-book "dg-list")

(defun cmp-d-ls-dgop-do (d p rsl)
  (cond ((endp p) (reverse rsl))
        ((< d (car p)) (cmp-d-ls-dgop-do d (cdr p) (cons (1- (car p)) rsl)))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) (append (reverse rsl) (rest p)))
        (t (cmp-d-ls-dgop-do (1- d) (cdr p) (cons (car p) rsl)))
        )
  )

(defun cmp-d-ls-d-do (d p)
  (cond ((endp p) d)
	((< d (car p)) (cmp-d-ls-d-do d (cdr p) ))
        ((and (<= 0 (- d (car p)))
              (<= (- d (car p)) 1)) nil)
        (t (cmp-d-ls-d-do (1- d) (cdr p)))
        )
  )

(defun cmp-d-ls (d ls)
  (cmp-d-ls-dgop-do d ls nil)
  )


(encapsulate
 ()
 
 (local
  (defthm append-revappend
      (equal (append (revappend l1 l2) l3)
             (revappend l1 (append l2 l3)))))
 
 (local
  (defthm revappend-append
      (equal (revappend (append ls1 ls2) ls3)
             (revappend ls2 (revappend ls1 ls3)))))
 
 (local
  (defthm cmp-d-ls-dgop-do-append-rsl
      (implies (and (true-listp rsl1)
                    (true-listp rsl2))
               (equal (cmp-d-ls-dgop-do s p (append rsl1 rsl2))
                      (append (reverse rsl2) (cmp-d-ls-dgop-do s p rsl1))))
    :rule-classes nil))
 
 (local
  (defthm cmp-d-ls-dgop-do-nil-rsl
      (implies (and (true-listp rsl1)
                    (not (endp rsl1)))
               (equal (cmp-d-ls-dgop-do s p rsl1)
                      (append (reverse rsl1) (cmp-d-ls-dgop-do s p nil))))
    :hints (("Goal" :use (:instance cmp-d-ls-dgop-do-append-rsl
                                    (rsl1 nil)
                                    (rsl2 rsl1))))))
 
 (defthm cmp-d-ls-recursive
     (equal (cmp-d-ls d ls)
            (cond ((endp ls) nil)
                  ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls d (cdr ls))))
                  ((and (<= 0 (- d (car ls)))
                        (<= (- d (car ls)) 1)) (cdr ls))              
                  (t (cons (car ls) (cmp-d-ls (1- d) (cdr ls))))
                  ))
   :rule-classes :definition)
 
 (defun cmp-d-ls-induct (d ls)
   (cond 
	 ((endp ls) nil)
         ((< d (car ls)) (cons (1- (car ls)) (cmp-d-ls-induct d (cdr ls))))
         ((and (<= 0 (- d (car ls)))
               (<= (- d (car ls)) 1)) (cdr ls))              
         (t (cons (car ls) (cmp-d-ls-induct (- d 1) (cdr ls))))
         )
   )
 
 (in-theory (disable cmp-d-ls))
 
 )

(defthm cmp-d-ls-cmp-d-ls-induct
    (equal (cmp-d-ls i ls)
           (cmp-d-ls-induct i ls)))

;; Notar que si > j (1+ (car ls)) entonces cmp-d-ls-induct j ls es ls

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-induct j ls)
		  ls)))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help1-bis
  (implies (and (natp j) (dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))

(defthm cmp-d-induct-cmp-d-induct-case-1.3-help2-bis
  (implies (and (natp j) (dgl-p ls)
		(>=  j (car ls))
		(not (endp ls))
		(not (and (<= 0 (- j (car ls)))
			  (<= (- j (car ls)) 1)))
		) 
	   (equal (cmp-d-ls-d-do j ls)
		  (- j (len ls)))))

(defthm dgl-p-cmp-d-ls
    (implies (and (dgl-p dgl)
                  (natp n))
             (dgl-p (cmp-d-ls n dgl)))
  :hints (("Goal" :induct (cmp-d-ls-induct n dgl))))

(defthm cmp-d-ls-d-do-not-nil
  (implies (and (natp j) 
		(dgl-p ls)
		(> j (+ (car ls) 1))
		(not (endp ls))
		) 
	   (cmp-d-ls-d-do j ls)))


;;;------------------------------------------------------------
;;;
;;; Binary representation
;;;
;;;------------------------------------------------------------


(include-book "dg-binary")

(include-book "binary-remove-zeros")

(defun 1dlop-dgop-binary (d dgop)
  (declare (xargs :measure (len dgop)))
  (if (and (natp d) (dgb-p dgop))
      (cond ((endp dgop) nil)
	    ((and (= d 1) (= (car dgop) 1)) (cdr dgop))
	    ((= d 0) (cdr dgop))
	    (t (cons (car dgop) (1dlop-dgop-binary (- d 1) (cdr dgop))))
	    )
    nil))
 

(defun final-1dlop-dgop-binary (d dgop)
  (remove-final-zeros (1dlop-dgop-binary d dgop)))


(defthm cmp-d-ls-induct-d=0-1+ls
  (implies (and (= d 0)
		(dgl-p dgop))
	   (equal (cmp-d-ls-induct d (1+ls dgop))
		  dgop)))

(defthm cmp-d-ls-induct-d=0-1+ls-bis
  (implies (and (= d 0)
		(dgb-p dgop))
	   (equal (cmp-d-ls-induct d (1+ls (dgb->dgl dgop)))
		  (dgb->dgl dgop)))
:hints (("Goal" :do-not-induct t 
	 :use ((:instance cmp-d-ls-induct-d=0-1+ls
			  (dgop (dgb->dgl dgop)))))))

(defun 1-ls (lst)
  (cond ((endp lst) nil)
	((= 0 (car lst)) nil)
	(t (cons (1- (car lst))
		 (1-ls (cdr lst))))))

(defthm 1-ls-1+ls=dgop
  (implies (dgl-p dgop)
	   (equal (1-ls (1+ls dgop))
		  dgop)))

(defthm cmp-d-ls-induct-d=0-is-equal-to-1-ls
  (implies (and (= d 0)
		(dgl-p dgop))
	   (equal (cmp-d-ls-induct d dgop)
		  (1-ls dgop))))


(defthm car=0-of-dgl-p
  (implies (and (dgl-p dgop)
		(= 0 (car dgop)))
	   (equal dgop '(0)))
:rule-classes nil)

(defthm cmp-d-ls-induct-d=1-is-equal-to-1-ls
  (implies (and (= d 1)
		(dgl-p dgop))
	   (equal (cmp-d-ls-induct d (append (1+ls dgop) '(0)))
		  (1-ls (append (1+ls dgop) '(0))))))


(defthm 1-ls-append-1+ls-dgop-0-equal-dgop
  (implies (dgl-p dgop)
	   (equal (1-ls (append (1+ls dgop) '(0)))
		  dgop)))


(defthm 1-ls-append-1+ls-dgop-0-equal-dgop-bis
  (implies (dgb-p dgop)
	   (equal (1-ls (append (1+ls (dgb->dgl dgop)) '(0)))
		  (dgb->dgl dgop)))
:hints (("Goal" :do-not-induct t 
	 :use ((:instance 1-ls-append-1+ls-dgop-0-equal-dgop
			  (dgop (dgb->dgl dgop))))))
)

(defthm dgl-p-append-1+ls-dgop-0
  (implies (dgl-p dgop)
	   (dgl-p (append (1+ls dgop) '(0)))))

(defthm cmp-d-ls-induct-d=0-append-1+ls-dgop-0-equal-dgop
  (implies (and (= d 0) (dgb-p dgop))
	   (equal (cmp-d-ls-induct d (append (1+ls (dgb->dgl dgop)) '(0)))
		  (dgb->dgl dgop)))
)

(defthm cdr-1+ls=1+ls-cdr
  (implies (dgl-p dgop)
	   (equal (cdr (1+ls dgop))
		  (1+ls (cdr dgop)))))

(defthm car-1+ls=1+car
  (implies (and (dgl-p dgop) (not (endp dgop)))
	   (equal (car (1+ls dgop))
		  (1+ (car dgop)))))

(defthm 1-car-1+ls=car
  (implies (and (dgl-p dgop) (not (endp dgop)))
	   (equal (1- (car (1+ls dgop)))
		  (car dgop))))

(defun cmp-d-ls-induct-4 (d ls)
  (declare (xargs :measure (len ls)))
   (cond 
	 ((endp ls) nil)
         ((< (- d 1) (car ls)) (cons (1- (car ls)) (cmp-d-ls-induct-4 d (cdr ls))))
         ((and (<= 0 (- (- d 1) (car ls)))
               (<= (- (- d 1) (car ls)) 1)) (cdr ls))              
         (t (cons (car ls) (cmp-d-ls-induct-4 (- d 1) (cdr ls))))
         )
   )

;;; We use the correct inductive schema
(defthm cmp-d-ls-induct-d+1+ls=1+ls-cmp-d-ls-induct-d-1
  (implies (and (natp d)
		(not (equal d 0))
		(dgl-p dgop))
	   (equal (cmp-d-ls-induct d (1+ls dgop))
		  (1+ls (cmp-d-ls-induct (- d 1) dgop))))
:hints (("Goal" :induct (cmp-d-ls-induct-4 d dgop)))
)

(defthm append-cmp-d-ls-induct-d+1+ls=1+ls-cmp-d-ls-induct-d-1
  (implies (and (natp d)
		(not (equal d 0))
		(not (equal d 1))
		(dgl-p dgop))
	   (equal (cmp-d-ls-induct d (append (1+ls dgop) '(0)))
		  (append (1+ls (cmp-d-ls-induct (- d 1) dgop)) '(0))))
:hints (("Goal" :induct (cmp-d-ls-induct-4 d dgop)))
)


(defthm 1dlop-dgop-binary-cmp-d-ls-induct
  (implies (and (natp d) (dgb-p dgop))
	   (equal (cmp-d-ls-induct d (dgb->dgl dgop))
		  (dgb->dgl (1dlop-dgop-binary d dgop)))))

(defthm 1dlop-dgop-binary-cmp-d-ls-induct/a
  (implies (and (natp d) (dgb-p dgop))
	   (equal (dgb->dgl (1dlop-dgop-binary d dgop))
		  (cmp-d-ls-induct d (dgb->dgl dgop))
		  )))

(in-theory (disable 1dlop-dgop-binary-cmp-d-ls-induct))

(in-theory (disable 1dlop-dgop-binary-cmp-d-ls-induct/a))

(defthm 1dlop-dgop-binary-cmp-d-ls-induct/b
  (implies (and (natp d) (dgb-p dgop))
	   (equal (dgl->dgb (dgb->dgl (1dlop-dgop-binary d dgop)))
		  (dgl->dgb (cmp-d-ls-induct d (dgb->dgl dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop-binary-cmp-d-ls-induct/a)))))

(in-theory (disable 1dlop-dgop-binary-cmp-d-ls-induct/b))


(defthm quasi-dgb-p-1dlop-dgop-binary
  (implies (and (natp d) (dgb-p dgop))
	   (quasi-dgb-p (1dlop-dgop-binary d dgop))))
	   


(defthm 1dlop-dgop-binary-cmp-d-ls-induct/c
  (implies (and (natp d) (dgb-p dgop))
	   (equal (dgl->dgb (dgb->dgl 
			     (remove-final-zeros (1dlop-dgop-binary d dgop))))
		  (dgl->dgb (cmp-d-ls-induct d (dgb->dgl dgop)))
		  ))
:hints 
(("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop-binary-cmp-d-ls-induct/b)
	       (:instance dgb->dgl-remove-final-zeros 
			  (dgop (1dlop-dgop-binary d dgop))))))
)


(defthm 1dlop-dgop-binary-cmp-d-ls-induct/d
  (implies (and (natp d) (dgb-p dgop))
	   (equal (remove-final-zeros (1dlop-dgop-binary d dgop))
		  (dgl->dgb (cmp-d-ls-induct d (dgb->dgl dgop)))
		  ))
:hints 
(("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop-binary-cmp-d-ls-induct/c)
	       (:instance quasi-dgb-p-1dlop-dgop-binary)
	       (:instance quasi-dgb-to-dgb
		(dgb (1dlop-dgop-binary d dgop)))
	       (:instance dgl->dgb-dgb->dgl (dgb (remove-final-zeros (1dlop-dgop-binary d dgop))))
	       )))
)



(defthm final-1dlop-dgop-binary-cmp-d-ls-induct
  (implies (and (natp d) (dgb-p dgop))
	   (equal (final-1dlop-dgop-binary d dgop)
		  (dgl->dgb (cmp-d-ls-induct d (dgb->dgl dgop)))
		  ))
:hints 
(("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop-binary-cmp-d-ls-induct/d)
	       ))))

;;;------------------------------------------------------------
;;;
;;; Kenzo representation
;;;
;;;------------------------------------------------------------

(include-book "dg-natural")

(include-book "arithmetic-4/top" :dir :system)

(include-book "logbitp")

(defun 1dlop-dgop (d dgop)
  (if (and (natp d) (natp dgop))
      (cond ((logbitp d dgop)	
	     (logxor (logand (ash -1 d)
			 (ash dgop -1))
		     (logandc1 (ash -1 d)
			       dgop)))
	    ((and (> d 0) (logbitp (- d 1) dgop))
	     (logxor (logand (ash (ash -1 d) -1)
			     (ash dgop -1))
		     (logandc1 (ash (ash -1 d) -1)
			       dgop)))
	    (t (logxor (logandc1 (ash -1 d) dgop)
		       (logand (ash -1 d) (ash dgop -1)))))
    nil))




;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  1dlop-dgop= 1dlop-dgop-binary
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



(defthm case-1/3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (and (= d 1) (= (car dgop) 1)))
		(= d 0)
		)
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop)))))



(defthm case-1/2-1-a
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		)
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (dgb->dgn (cdr dgop)))))


(defthm case-1/2-1-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(not (logbitp 1 (dgb->dgn dgop)))
		(logbitp 0 (dgb->dgn dgop))
		)
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash (ash -1 d) -1)
			     (ash (dgb->dgn dgop) -1))
		     (logandc1 (ash (ash -1 d) -1)
			       (dgb->dgn dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop 
			  (dgop (dgb->dgn dgop)))))))



(defthm case-1/2-1-c
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(= (cadr dgop) 0)
		)
	   (equal (logxor (logand (ash (ash -1 d) -1)
			     (ash (dgb->dgn dgop) -1))
		     (logandc1 (ash (ash -1 d) -1)
			       (dgb->dgn dgop)))
		  (dgb->dgn (cdr dgop))
		  )))


(defthm case-1/2-1-d
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(= (cadr dgop) 0)
		)
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (dgb->dgn (cdr dgop))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance cadr-dgop=0-car-dgop=1=>logbitp-0)
	       (:instance cadr-dgop=0-car-dgop=1=>not-logbitp-1)
	       (:instance case-1/2-1-b)
	       (:instance case-1/2-1-c))
	 )))

(defthm case-1/2-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(= (cadr dgop) 0)
		)
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/2-1-d)
	       (:instance case-1/2-1-a))
	 )))


(defthm case-1/2-2-a
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(logbitp 1 (dgb->dgn dgop))
		)
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 d)
			 (ash (dgb->dgn dgop)  -1))
		     (logandc1 (ash -1 d)
			       (dgb->dgn dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop 
			  (dgop (dgb->dgn dgop)))))))



(defthm case-1/2-2-b-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(= (cadr dgop) 1)
		)
	   (equal (logxor (logand (ash -1 d)
			 (ash (dgb->dgn dgop)  -1))
		     (logandc1 (ash -1 d)
			       (dgb->dgn dgop)))
		  (logxor (logand -2
			 (ash (+ 1 (ash (dgb->dgn (cdr dgop)) 1))  -1))
		     (logandc1 -2
			       (dgb->dgn dgop)))
		  )))

(defthm car=1->oddp-dgb->dgn
  (implies (and (dgb-p dgb)
		(= (car dgb) 1))
	   (oddp (dgb->dgn dgb)))
:hints (("Goal"  :in-theory (enable oddp evenp))))


(defthm car=1->oddp-dgb->dgn-bis
  (implies (= (car dgb) 1)
	   (oddp (dgb->dgn dgb)))
:hints (("Goal"  :in-theory (enable oddp evenp))))

(defthm logandc1--2-oddp-b
  (implies (and (natp n)
		(oddp n))
	   (equal (logandc1 -2 n)
		  1))
:hints (("Goal"  :in-theory (enable logand oddp evenp)))
)


(defthm case-1/2-2-b-2
  (implies (and (dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1))
	   (equal (logandc1 -2 (dgb->dgn dgop)) 1))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance car=1->oddp-dgb->dgn (dgb dgop))
		 (:instance logandc1--2-oddp-b (n (dgb->dgn dgop)))))))



(defthm case-1/2-2-b-3
  (implies (and (dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1))
	   (equal (ash (+ 1 (ash (dgb->dgn (cdr dgop)) 1))  -1) 
		  (dgb->dgn (cdr dgop))))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance ash-1-1-1 (n (dgb->dgn (cdr dgop))))
		 (:instance natp-dgb->dgn (dgb (cdr dgop)))
		 ))))


(defthm case-1/2-2-b-4
  (implies (= (cadr dgop) 1)
	   (oddp (dgb->dgn (cdr dgop)))
	   )
  :hints (("Goal" :do-not-induct t
	   :use ((:instance car=1->oddp-dgb->dgn-bis
			    (dgb (cdr dgop)))
		 ))))


(defthm logand--2-oddp-bis
  (implies (and (natp n)
		(oddp n))
	   (equal (logand -2 n)
		  (- n 1)))
:hints (("Goal"  :in-theory (enable logand oddp evenp)))
)

(DEFTHM DGB-P=>DGB-P-CDR
  (IMPLIES (DGB-P DGOP)
	   (DGB-P (CDR DGOP))))

(defthm case-1/2-2-b-5
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(= (cadr dgop) 1)
		)
	   (equal (logand -2 (ash (+ 1 (ash (dgb->dgn (cdr dgop)) 1))  -1))
		  (- (dgb->dgn (cdr dgop)) 1)
	     ))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance case-1/2-2-b-3)
		 (:instance case-1/2-2-b-4)
		 (:instance logand--2-oddp-bis
			    (n (dgb->dgn (cdr dgop))))
		 ))))


(DEFTHM LOGXOR-ODDP
  (IMPLIES (AND (NATP N) (ODDP N))
	   (EQUAL (LOGXOR (- N 1) 1) N))
  :hints (("Goal" :in-theory (enable evenp))))

(defthm case-1/2-2-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(= (cadr dgop) 1)
		)
	   (equal (logxor (logand (ash -1 d)
			 (ash (dgb->dgn dgop)  -1))
		     (logandc1 (ash -1 d)
			       (dgb->dgn dgop)))
		  (dgb->dgn (cdr dgop))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/2-2-b-1)
	       (:instance case-1/2-2-b-5)
	       (:instance case-1/2-2-b-2)
	       (:instance case-1/2-2-b-4)
	       (:instance logxor-oddp
			  (n (dgb->dgn (cdr dgop))))
	       ))))


(defthm case-1/2-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		(= (cadr dgop) 1)
		)
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/2-1-a)
	       (:instance cadr-dgop=1=>logbitp-1)
	       (:instance case-1/2-2-a)
	       (:instance  case-1/2-2-b)
	       ))))




(defthm case-1/2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(and (= d 1) (= (car dgop) 1))
		)
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary dgb->dgn
			     1dlop-dgop)
	 :use ((:instance case-1/2-1)
	       (:instance case-1/2-2)
	       ))))
		     
;;; First question

(defthm case-1/4-0-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (and (= d 1) (= (car dgop) 1)))
		(not (= d 0))
		)
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (dgb->dgn (cons (car dgop) (1dlop-dgop-binary (- d 1) (cdr dgop))))))
:hints (("Goal" :do-not-induct t 
	 :use ((:instance 1dlop-dgop-binary)))))

(defthm case-1/4-0-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (and (= d 1) (= (car dgop) 1)))
		(not (= d 0))
		)
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (+ (car dgop) (ash (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop))) 1))))
:hints (("Goal" :do-not-induct t 
	 :use ((:instance case-1/4-0-1)))))

(defthm natp-not-0-natp-d-1
  (implies (and (natp d)
		(not (= d 0)))
	   (natp (+ -1 d))))


(defthm case-1/4-0-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (and (= d 1) (= (car dgop) 1)))
		(not (= d 0))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				))
:hints (("Goal" :do-not-induct t 
	 :use ((:instance natp-not-0-natp-d-1)
	       (:instance dgb-p=>dgb-p-cdr)
	       ))))

(defthm case-1/4-0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (and (= d 1) (= (car dgop) 1)))
		(not (= d 0))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (+ (car dgop) (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))))
:hints (("Goal" :do-not-induct t 
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-0-3)
	       (:instance case-1/4-0-2)))))



;;; Case 1. We suppose that (= (car dgop) 0)

;;; Case 1.a (logbitp d (dgb->dgn dgop)) => (logbitp (- d 1) (dgb->dgn (cdr dgop)))

(defthm my-logbitp-d=>my-lobitp-d-1
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 0)
		(my-logbitp d dgop))
	   (my-logbitp (- d 1) (cdr dgop))))


(defthm logbitp-d=>logbitp-d-1-b
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 0)
		(logbitp d (dgb->dgn dgop)))
	   (logbitp (- d 1) (dgb->dgn (cdr dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-d=>my-lobitp-d-1)
	       (:instance my-logbitp-logbitp-b)
	       (:instance my-logbitp-logbitp-b (d (- d 1)) (dgop (cdr dgop))))))
)
	   
(defthm case-1/4-1-a-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 d)
			 (ash (dgb->dgn dgop) -1))
		     (logandc1 (ash -1 d)
			       (dgb->dgn dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (dgop (dgb->dgn dgop)))
	       ))))


(defthm case-1/4-1-a-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 d)
			       (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-1-a-1))
	       )))




(defthm case-1/4-1-a-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
		  (logxor (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
		     (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (d (- d 1))
			  (dgop (dgb->dgn (cdr dgop)))))
	       )))


(defthm natp-logand-ash
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(natp n)
		)
	   (natp (logand (ash -1 (- d 1))
			 (ash n -1))))
:hints (("Goal" :in-theory (enable expt ash logand))))

(defthm natp-logand-ash-dgb->dgn-cdr
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (natp (logand (ash -1 (- d 1))
			 (ash (dgb->dgn (cdr dgop))  -1))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance natp-logand-ash (n (dgb->dgn (cdr dgop))))))))

(defthm natp-logandc1-ash
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(natp n)
		)
	   (natp (logandc1 (ash -1 (- d 1))
			 n)))
:hints (("Goal" :in-theory (enable expt ash logand))))

(defthm natp-logandc1-ash-dgb->dgn-cdr
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (natp (logandc1 (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)) )))
:hints (("Goal" :do-not-induct t
	 :use ((:instance natp-logandc1-ash (n (dgb->dgn (cdr dgop))))))))

(defthm case-1/4-1-a-4-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (ash (logxor (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
			  (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))) 1)
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-1-a-3)
	       ))))

(defthm case-1/4-1-a-4-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (logxor (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
			  (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))) 1)
		  (logxor (ash (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :use (
	       (:instance natp-logand-ash-dgb->dgn-cdr)
	       (:instance natp-logandc1-ash-dgb->dgn-cdr)
	       (:instance ash-logxor
			  (n1 (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1)))
			  (n2 (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))))))))


(defthm case-1/4-1-a-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-1-a-4-1)
	       (:instance case-1/4-1-a-4-2)
	        )
	       )))

(DEFTHM ASH-LOGAND-INTEGER
  (IMPLIES (AND (INTEGERP N1) (INTEGERP N2))
	   (EQUAL (ASH (LOGAND N1 N2) 1)
		  (LOGAND (ASH N1 1) (ASH N2 1))))
  :HINTS
  (("Goal"
    :IN-THEORY (ENABLE EVENP ASH LOGXOR
		       LOGEQV LOGNOT LOGORC1 LOGIOR LOGAND))))

(defthm case-1/4-1-a-5-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (ash (logand (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) -1)) 1)
		  (logand (ash  (ash -1 (- d 1)) 1)
			  (ash (ash (dgb->dgn (cdr dgop)) -1) 1))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logand-integer 
			  (n1 (ash -1 (- d 1)))
			  (n2 (ash (dgb->dgn (cdr dgop)) -1)))
	       )
	       )))


(defthm logand-ash-ash-integer
    (implies (and (integerp n) (natp d) (> d 0))
             (equal (logand (ash -1 d) n)
                    (logand (ash -1 d) (ash (ash n -1) 1))))
  :hints
  (("goal"
    :in-theory (enable evenp ash logxor
                       logeqv lognot logorc1 logior logand))))

(defthm case-1/4-1-a-5-1-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (ash (logand (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) -1)) 1)
		  (logand (ash -1 d)
			  (dgb->dgn (cdr dgop)))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-1-a-5-1)
	       (:instance logand-ash-ash-integer
			  (n (dgb->dgn (cdr dgop)))))
	       )))

(defthm ash-logandc1-integer
    (implies (and (integerp n1) (integerp n2))
             (equal (ash (logandc1 n1 n2) 1)
                    (logandc1 (ash n1 1) (ash n2 1))))
  :hints
  (("goal"
    :in-theory (enable evenp ash logxor
                       logeqv lognot logorc1 logior logand))))

(defthm case-1/4-1-a-5-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (ash (logandc1 (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop))) 1)
		  (logandc1 (ash (ash -1 (- d 1)) 1)
			    (ash (dgb->dgn (cdr dgop)) 1))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logandc1-integer 
			  (n1 (ash -1 (- d 1)))
			  (n2 (dgb->dgn (cdr dgop))))
	       )
	       )))

(defthm case-1/4-1-a-5-2-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (ash (logandc1 (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop))) 1)
		  
		  (logandc1 (ash -1 d)
			    (ash (dgb->dgn (cdr dgop)) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-1-a-5-2 )
	       )
	       )))


(defthm case-1/4-1-a-5-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (logxor (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-1-a-5-1-b)
	       (:instance case-1/4-1-a-5-2-b)
	       )
	       )))

(defthm equal-equal
  (implies (and (equal a b)
		(equal b c))
	   (equal a c))
  :rule-classes nil)


(defthm case-1/4-1-a-5
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash 1dlop-dgop logxor logbitp 
			     dgb->dgn logandc1)
	 :use ((:instance case-1/4-1-a-4)
	       (:instance case-1/4-1-a-5-3)
	       (:instance equal-equal 
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)))
			  (c (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))))
	       )
	       )))


(defthm case-1/4-1-a-6
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance logbitp-d=>logbitp-d-1-b)
	       (:instance case-1/4-1-a-5))
	       )))



(defthm case-1/4-1-a
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(logbitp d (dgb->dgn dgop))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-0 )
	       (:instance case-1/4-1-a-6)
	       (:instance case-1/4-1-a-2))
	       )))


;;; Case 1.b (logbitp (- d 1) (dgb->dgn dgop)) => (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))
;;; 1.b.1 (> d 1)
;;; 1.b.2 (= d 1)

(defthm my-logbitp-d>1=>my-lobitp-d-1
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 1)
		(my-logbitp (- d 1) dgop))
	   (my-logbitp (- (- d 1) 1) (cdr dgop))))


(defthm logbitp-d>1=>logbitp-d-1
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 1)
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-d>1=>my-lobitp-d-1)
	       (:instance my-logbitp-logbitp-b (d (- d 1)))
	       (:instance my-logbitp-logbitp-b (d (- (- d 1) 1)) (dgop (cdr dgop))))))
)

(defthm not-my-logbitp-d=>not-my-lobitp-d-1
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 0)
		(not (my-logbitp d dgop)))
	   (not (my-logbitp (- d 1) (cdr dgop)))))

(defthm not-logbitp-d>1=>not-logbitp-d-1
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 0)
		(not (logbitp d (dgb->dgn dgop))))
	   (not (logbitp (- d 1) (dgb->dgn (cdr dgop)))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-my-logbitp-d=>not-my-lobitp-d-1)
	       (:instance my-logbitp-logbitp-b)
	       (:instance my-logbitp-logbitp-b (d (- d 1)) (dgop (cdr dgop))))))
)


(defthm case-1/4-1-b-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop))
		)
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash (ash -1 d) -1)
			     (ash (dgb->dgn dgop)  -1))
		     (logandc1 (ash (ash -1 d) -1)
			       (dgb->dgn dgop)))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (dgop (dgb->dgn dgop)))
	       ))))

(defthm ash-1-d-1
  (implies (and (natp d) (> d 0))
	   (equal (ash (ash -1 d) -1)
		  (ash -1 (- d 1)))))

(defthm dgb-p-dgop-not-car=1-implies
  (implies (and (dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1)))
	   (equal (ash (dgb->dgn dgop)  -1)
		  (dgb->dgn (cdr dgop)))))
		

(defthm equal-expt-2-d-1
  (implies (and (natp d) (> d 0))
	   (equal (- (EXPT 2 (+ -1 D)))
		  (- (/ (EXPT 2 (+ 1 (- D))))))))
	   


(defthm case-1/4-1-b-2-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (logand (ash (ash -1 d) -1)
			  (ash (dgb->dgn dgop)  -1))
		  (logand (ash -1 (- d 1))
			  (dgb->dgn (cdr dgop)))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash)
	 :use ((:instance ash-1-d-1)
	       (:instance dgb-p-dgop-not-car=1-implies))))
)

(defthm case-1/4-1-b-2-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (logandc1 (ash (ash -1 d) -1)
			       (dgb->dgn dgop))
		  (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash)
	 :use ((:instance ash-1-d-1)
	       )))
)



(defthm case-1/4-1-b-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop))
		)
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-1-b-1)
	       (:instance case-1/4-1-b-2-1)
	       (:instance case-1/4-1-b-2-2)
	       ))))



(defthm case-1/4-1-b-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))
		)
	   (equal (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
		  (logxor (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1))
		     (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (d (- d 1))
			  (dgop (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-1-b-4-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))
		)
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (ash (logxor (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1))
		     (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop)))) 1)
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-1-b-3)
	       ))))

(defthm case-1/4-1-b-4-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))
		)
	   (equal (ash (logxor (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1))
		     (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop)))) 1)
		  (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :use (
	       (:instance natp-logand-ash-dgb->dgn-cdr)
	       (:instance natp-logandc1-ash-dgb->dgn-cdr)
	       (:instance ash-logxor
			  (n1 (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)))
			  (n2 (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop)))))))))



(defthm case-1/4-1-b-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-1-b-4-1)
	       (:instance case-1/4-1-b-4-2)
	        )
	       )))



(defthm case-1/4-1-b-5-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
		  (logand (ash (ash (ash -1 (- d 1)) -1) 1)
			  (ash (ash (dgb->dgn (cdr dgop))  -1) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logand-integer 
			  (n1 (ash (ash -1 (- d 1)) -1))
			  (n2 (ash (dgb->dgn (cdr dgop)) -1)))
	       )
	       )))



(defthm case-1/4-1-b-5-1-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
		  (logand (ash -1 (- d 1))
			  (dgb->dgn (cdr dgop)))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-1-b-5-1)
	       (:instance logand-ash-ash-integer
			  (d (- d 1))
			  (n (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-1-b-5-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1)
		  (logandc1 (ash (ash (ash -1 (- d 1)) -1) 1)
			       (ash (dgb->dgn (cdr dgop)) 1))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logandc1-integer 
			  (n1 (ash (ash -1 (- d 1)) -1))
			  (n2 (dgb->dgn (cdr dgop))))
	       )
	       )))

(defthm case-1/4-1-b-5-2-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1)
		  (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-1-b-5-2 )
	       )
	       )))


(defthm case-1/4-1-b-5-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		)
	   (equal (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-1-b-5-1-b)
	       (:instance case-1/4-1-b-5-2-b)
	       )
	       )))


(defthm case-1/4-1-b-5
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash 1dlop-dgop logxor logbitp 
			     dgb->dgn logandc1)
	 :use ((:instance case-1/4-1-b-4)
	       (:instance case-1/4-1-b-5-3)
	       (:instance equal-equal 
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1)))
			  (c (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )))
	       )
	       )))



(defthm case-1/4-1-b-6
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance logbitp-d>1=>logbitp-d-1)
	       (:instance not-logbitp-d>1=>not-logbitp-d-1)
	       (:instance case-1/4-1-b-5))
	       )))




(defthm case-1/4-1-b.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-0 )
	       (:instance case-1/4-1-b-6)
	       (:instance case-1/4-1-b-2))
	       )))



(defthm d=1-my-logbitp-d-1=>car=1
  (implies (and (= d 1)
		(my-logbitp (- d 1) dgop))
	   (equal (car dgop) 1)))

(defthm d=1-logbitp-d-1=>car=1
  (implies (and (= d 1)
		(dgb-p dgop)
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (car dgop) 1))
  :hints (("Goal" :do-not-induct t
	   :use ((:instance my-logbitp-logbitp-b
			    (d (- d 1)))
		 (:instance d=1-my-logbitp-d-1=>car=1)
			    ))))

(defthm case-1/4-1-b.2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(= d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance d=1-logbitp-d-1=>car=1)
	       )
	       )))


(defthm case-1/4-1-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-1-b.1)
	       (:instance case-1/4-1-b.2)
	       )
	       )))


;;; Case 1.c (not (logbitp (- d 1) (dgb->dgn dgop))) => (not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop))))

(defthm not-my-logbitp-d-1=>not-my-lobitp-d-1-1
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 0)
		(not (my-logbitp (- d 1) dgop)))
	   (not (my-logbitp (- (- d 1) 1) (cdr dgop)))))


(defthm not-my-logbitp-not-logbitp-b
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (not (my-logbitp d dgop))
		  (not (logbitp d (dgb->dgn dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use
	 ((:instance my-logbitp-logbitp (dgop (dgb->dgn dgop)))))))

(defthm not-logbitp-d-1=>not-logbitp-d-1-1
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 0)
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable logbitp dgb->dgn)
	 :use ((:instance not-my-logbitp-d-1=>not-my-lobitp-d-1-1)
	       (:instance not-my-logbitp-not-logbitp-b (d (- d 1)))
	       (:instance not-my-logbitp-not-logbitp-b (d (- (- d 1) 1)) (dgop (cdr dgop))))))
)


(defthm case-1/4-1-c-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logandc1 (ash -1 d)
			       (dgb->dgn dgop))
			  (logand (ash -1 d)
			 (ash (dgb->dgn dgop) -1))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (dgop (dgb->dgn dgop)))
	       ))))


(defthm case-1/4-1-c-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logandc1 (ash -1 d)
			       (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-1-c-1))
	       )))

(defthm natp-dgb->dgn-2
  (implies (dgb-p (cdr dgop))
	   (natp (dgb->dgn (cdr dgop)))))

(defthm integer-dgb->dgn
  (implies (dgb-p (cdr dgop))
	   (integerp (dgb->dgn (cdr dgop))))
:hints (("Goal" :use ((:instance  NATP-DGB->DGN-2)))))


(defthm case-1/4-1-c-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
		  (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			  (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (d (- d 1))
			  (dgop (dgb->dgn (cdr dgop)))))
	       )))

(defthm case-1/4-1-c-3.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(= d 1))
	   (equal (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
		  (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			  (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (d (- d 1))
			  (dgop (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-1-c-4-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (ash (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			(logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
			  ) 1)
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-1-c-3)
	       ))))

(defthm case-1/4-1-c-4-1.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(= d 1))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (ash (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			(logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
			  ) 1)
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-1-c-3.1)
	       ))))

(defthm case-1/4-1-c-4-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			       (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))) 1)
		  (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
			  (ash (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1)) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :use (
	       (:instance natp-logand-ash-dgb->dgn-cdr)
	       (:instance natp-logandc1-ash-dgb->dgn-cdr)
	       (:instance ash-logxor
			  (n1 (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop))))
			  (n2 (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))))))))

(defthm case-1/4-1-c-4-2.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(= d 1))
	   (equal (ash (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			       (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))) 1)
		  (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
			  (ash (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1)) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :use (
	       (:instance natp-logand-ash-dgb->dgn-cdr)
	       (:instance natp-logandc1-ash-dgb->dgn-cdr)
	       (:instance ash-logxor
			  (n1 (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop))))
			  (n2 (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))))))))


(defthm case-1/4-1-c-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  )
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-1-c-4-1)
	       (:instance case-1/4-1-c-4-2)
	        )
	       )))

(defthm case-1/4-1-c-4.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(= d 1))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  )
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-1-c-4-1.1)
	       (:instance case-1/4-1-c-4-2.1)
	        )
	       )))




(defthm case-1/4-1-c-5-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		)
	   (equal (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  )
		  (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-1-a-5-1-b)
	       (:instance case-1/4-1-a-5-2-b)
	       )
	       )))

(defthm case-1/4-1-c-5
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash 1dlop-dgop logxor logbitp 
			     dgb->dgn logandc1)
	 :use ((:instance case-1/4-1-c-4)
	       (:instance case-1/4-1-c-5-3)
	       (:instance equal-equal 
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  ))
			  (c (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))))
	       )
	       )))

(defthm case-1/4-1-c-5.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(= d 1))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash 1dlop-dgop logxor logbitp 
			     dgb->dgn logandc1)
	 :use ((:instance case-1/4-1-c-4.1)
	       (:instance case-1/4-1-c-5-3)
	       (:instance equal-equal 
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  ))
			  (c (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))))
	       )
	       )))


(defthm case-1/4-1-c-6
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-logbitp-d>1=>not-logbitp-d-1)
	       (:instance not-logbitp-d-1=>not-logbitp-d-1-1)
	       (:instance case-1/4-1-c-5))
	       )))

(defthm case-1/4-1-c-6.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(= d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-logbitp-d>1=>not-logbitp-d-1)
	       (:instance case-1/4-1-c-5.1))
	       )))

(defthm case-1/4-1-c-6.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-1-c-6)
	       (:instance case-1/4-1-c-6.1))
	       )))

(defthm case-1/4-1-c
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop)))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-0 )
	       (:instance case-1/4-1-c-6.0)
	       (:instance case-1/4-1-c-2))
	       )
	       ))



(defthm case-1/4-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-1-a )
	       (:instance case-1/4-1-b)
	       (:instance case-1/4-1-c))
	       )))


;;; Case 2. We suppose that (> d 1)

;;; Case 2.a  Supongamos que (car dgop) = 0
;;; Se tiene entonces el resultado por todo lo demostrado anteriormente


(defthm case-1/4-2.a
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= (car dgop) 1))
		(not (= d 0))
		(> d 1)
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-1 )
	       )
	       )))

;;; Case 2.b Supongamos que (car dgop) = 1

;;; Una cuestion previa

;;; Case 2.b.1 (logbitp d (dgb->dgn dgop))

(defthm case-1/4-2-a-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 d)
			 (ash (dgb->dgn dgop) -1))
		     (logandc1 (ash -1 d)
			       (dgb->dgn dgop)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (dgop (dgb->dgn dgop)))
	       ))))

(defthm case-1/4-2-a-2.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 d)
				  (ash (+ 1 (ash (dgb->dgn (cdr dgop)) 1)) -1))
		     (logandc1 (ash -1 d)
			       (+ 1 (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	  :use ((:instance case-1/4-2-a-1))
	       )))

(defthm case-1/4-2-a-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 d)
			       (+ 1 (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	  :use ((:instance case-1/4-2-a-2.0)
		(:instance ash-1-1-1 (n (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-2-a-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
		  (logxor (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
		     (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (d (- d 1))
			  (dgop (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-2-a-4-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (ash (logxor (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
			  (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))) 1)
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-3)
	       ))))

(defthm natp-logand-ash-2
  (implies (and (natp d) 
		(not (= d 0))
		(natp n)
		)
	   (natp (logand (ash -1 (- d 1))
			 (ash n -1))))
:hints (("Goal" :in-theory (enable expt ash logand))))

(defthm natp-logand-ash-dgb->dgn-cdr-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= d 0))
		)
	   (natp (logand (ash -1 (- d 1))
			 (ash (dgb->dgn (cdr dgop))  -1))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance natp-logand-ash-2 (n (dgb->dgn (cdr dgop))))))))

(defthm natp-logandc1-ash-2
  (implies (and (natp d) 
		(not (= d 0))
		(natp n)
		)
	   (natp (logandc1 (ash -1 (- d 1))
			 n)))
:hints (("Goal" :in-theory (enable expt ash logand))))

(defthm natp-logandc1-ash-dgb->dgn-cdr-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= d 0))
		)
	   (natp (logandc1 (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)) )))
:hints (("Goal" :do-not-induct t
	 :use ((:instance natp-logandc1-ash-2 (n (dgb->dgn (cdr dgop))))))))



(defthm case-1/4-2-a-4-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (logxor (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
			  (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))) 1)
		  (logxor (ash (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :use (
	       (:instance natp-logand-ash-dgb->dgn-cdr-2)
	       (:instance natp-logandc1-ash-dgb->dgn-cdr-2)
	       (:instance ash-logxor
			  (n1 (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1)))
			  (n2 (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))))))))


(defthm case-1/4-2-a-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-2-a-4-1)
	       (:instance case-1/4-2-a-4-2)
	        )
	       )))


(defthm case-1/4-2-a-5-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (ash (logand (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) -1)) 1)
		  (logand (ash  (ash -1 (- d 1)) 1)
			  (ash (ash (dgb->dgn (cdr dgop)) -1) 1))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logand-integer 
			  (n1 (ash -1 (- d 1)))
			  (n2 (ash (dgb->dgn (cdr dgop)) -1)))
	       )
	       )))



(defthm case-1/4-2-a-5-1-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (ash (logand (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) -1)) 1)
		  (logand (ash -1 d)
			  (dgb->dgn (cdr dgop)))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-2-a-5-1)
	       (:instance logand-ash-ash-integer
			  (n (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-2-a-5-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (ash (logandc1 (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop))) 1)
		  (logandc1 (ash (ash -1 (- d 1)) 1)
			    (ash (dgb->dgn (cdr dgop)) 1))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logandc1-integer 
			  (n1 (ash -1 (- d 1)))
			  (n2 (dgb->dgn (cdr dgop))))
	       )
	       )))

(defthm case-1/4-2-a-5-2-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (ash (logandc1 (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop))) 1)
		  
		  (logandc1 (ash -1 d)
			    (ash (dgb->dgn (cdr dgop)) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-2-a-5-2 )
	       )
	       )))



(defthm case-1/4-2-a-5-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (logxor (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-2-a-5-1-b)
	       (:instance case-1/4-2-a-5-2-b)
	       )
	       )))




(defthm case-1/4-2-a-5
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp (- d 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash 1dlop-dgop logxor logbitp 
			     dgb->dgn logandc1)
	 :use ((:instance case-1/4-2-a-4)
	       (:instance case-1/4-2-a-5-3)
	       (:instance equal-equal 
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)))
			  (c (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))))
	       )
	       )))

(defthm case-1/4-2-a-6
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance logbitp-d=>logbitp-d-1-b)
	       (:instance case-1/4-2-a-5))
	       )))

(defthm equal+1
  (implies (equal a b)
	   (equal (+ 1 a) (+ 1 b)))
:rule-classes nil)

(defthm case-1/4-2-a-6.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (+ 1 (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-6)
	       (:instance equal+1
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))))
	       )
	       )))


(defthm logand-ash-evenp
  (implies (and (natp d)
		(> d 0)
		(natp a))
	   (evenp (logand (ash -1 d) a)))
:hints (("Goal" :in-theory (enable logand ash evenp))))

(defthm logandc1-ash-evenp-b
  (implies (and (natp d)
		(> d 0)
		(evenp a))
	   (evenp (logandc1 (ash -1 d) a)))
:hints (("Goal" :in-theory (enable logand ash evenp))))


(defthm case-1/4-2-a-7.1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (evenp (logand (ash -1 d) (dgb->dgn (cdr dgop)))))
	   
:hints (("Goal" :do-not-induct t
	 :in-theory (disable logandc1 logxor logand ash
			     dgb->dgn logbitp)
	 :use ((:instance natp-dgb->dgn-2)
	       (:instance logand-ash-evenp
			  (a (dgb->dgn (cdr dgop))))
	       ))))

(in-theory (disable LOGAND-ASH-ASH-INTEGER
		    ))

(defthm case-1/4-2-a-7.4-b
  (implies (and (natp d) 
		(natp a)
		(> d 1)
		(not (= d 0))
		)
	   (natp (logand (ash -1 d) a))))

(defthm case-1/4-2-a-7.4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (natp (logand (ash -1 d) (dgb->dgn (cdr dgop)))))
:hints (("Goal" :use ((:instance case-1/4-2-a-7.4-b
				 (a (dgb->dgn (cdr dgop))))))))
	   

(defthm case-1/4-2-a-7.2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (evenp (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))
	   
:hints (("Goal" :do-not-induct t
	 :in-theory (disable logandc1 logxor logand
			     dgb->dgn logbitp ash-to-floor)
	 :use ((:instance natp-dgb->dgn-2)
	       (:instance evenp-ash-n-1 (n (dgb->dgn (cdr dgop))))
	       (:instance logandc1-ash-evenp-b
			  (a (dgb->dgn (cdr dgop))))
	       ))))

(defthm case-1/4-2-a-7.3.0
  (implies (and (natp d) 
		(natp a)
		(> d 1)
		(not (= d 0))
		)
	   (natp (logandc1 (ash -1 d)
				  (ash a 1))))
	   )

(defthm case-1/4-2-a-7.3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (natp (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))
	   
  :hints (("Goal" :use ((:instance case-1/4-2-a-7.3.0
				   (a (dgb->dgn (cdr dgop))))))))


(in-theory (disable ash-to-floor))

(DEFTHM LOGXOR-1-EVEN
                 (IMPLIES (AND (EVENP N) (NATP N))
                          (EQUAL (LOGXOR 1 N) (+ 1 N)))
                 :HINTS
                 (("Goal"
                       :IN-THEORY (ENABLE LOGXOR LOGEQV LOGORC1
                                          LOGIOR LOGNOT LOGAND EXPT EVENP))))

(defthm logxor-evenp-evenp
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (evenp (logxor n1 n2)))
 :hints (("Goal" :in-theory (enable logxor logeqv evenp logand zip
				    logorc1))))

(defthm logxor-1-evenp-evenp-aux
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (+ 1 (logxor n1 n2))
		  (logxor 1 (logxor n1 n2))))
:hints (("Goal" :use ((:instance logxor-evenp-evenp)
		      (:instance logxor-1-even (n (logxor n1 n2)))))))

(defthm logxor-1-evenp-evenp-aux-2
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (logxor 1 (logxor n1 n2))
		  (logxor 1 n1 n2)))
:hints (("Goal" :in-theory (enable logxor evenp logand zip))))


(defthm logxor-1-evenp-evenp-aux-3
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (logxor 1 (logxor n1 n2))
		  (logxor (logxor 1 n1) n2 )
		  ))
:hints (("Goal" :use ((:instance logxor-asociativo 
				 (n1 1)
				 (n2 n1)
				 (n3 n2))))))

(defthm logxor-1-evenp-evenp-aux-4
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (logxor 1 (logxor n1 n2))
		  (logxor (+ 1 n1) n2 )
		  ))
:hints (("Goal" :use ((:instance logxor-1-evenp-evenp-aux-3)))))


(defthm logxor-1-evenp-evenp-aux-5
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (logxor 1 (logxor n1 n2))
		  (logxor (logxor n1 1) n2 )
		  ))
:hints (("Goal" :use ((:instance logxor-1-evenp-evenp-aux-3)
		      (:instance logxor-commutativo
				 (n1 1)
				 (n2 n1))))))

(defthm logxor-1-evenp-evenp-aux-6
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (logxor 1 (logxor n1 n2))
		  (logxor n1 (logxor 1 n2))
		  ))
:hints (("Goal" :use ((:instance logxor-1-evenp-evenp-aux-5)
		      (:instance logxor-asociativo
				 (n2 1)
				 (n3 n2))))))

(defthm logxor-1-evenp-evenp-aux-7
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (logxor 1 (logxor n1 n2))
		  (logxor n1 (1+ n2))
		  )))

(defthm logxor-1-evenp-evenp
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (+ 1 (logxor n1 n2))
		  (logxor n1 (1+ n2))))
  :hints (("Goal" :use ((:instance logxor-1-evenp-evenp-aux)
			(:instance logxor-1-evenp-evenp-aux-7)))))


(defthm case-1/4-2-a-7
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (+ 1 (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (1+ (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-7.1)
	       (:instance case-1/4-2-a-7.2)
	       (:instance case-1/4-2-a-7.3)
	       (:instance case-1/4-2-a-7.4)
	       (:instance logxor-1-evenp-evenp
			  (n1 (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))
			  (n2 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))))
	       )))

(defthm case-1/4-2-a-8
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (+ 1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-7)
	       (:instance case-1/4-2-a-6.0)
	       (:instance equal-equal
			  (a (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)))
			  (b (+ 1 (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))))
			  (c (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (+ 1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))))
	       ))))



(defthm evenp-ash-1-d
  (implies (and (natp d)
		(> d 1))
	   (evenp (ash -1 d)))
  :hints (("Goal" :in-theory (enable ash evenp))))

(defthm logandc1-1-evenp-evenp-b
  (implies (and	(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (+ 1 (logandc1 n1 n2))
		  (logandc1 n1 (1+ n2))))
 :hints (("Goal" :in-theory (enable logand evenp zip))))

(defthm case-1/4-2-a-9.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (+ 1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))) 
		  (logandc1 (ash -1 d)
				  (+ 1 (ash (dgb->dgn (cdr dgop)) 1))))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance evenp-ash-1-d)
	       (:instance natp-dgb->dgn-2)
	       (:instance evenp-ash-n-1 (n (dgb->dgn (cdr dgop))))
	       (:instance logandc1-1-evenp-evenp-b
			  (n1 (ash -1 d))
			  (n2 (ash (dgb->dgn (cdr dgop)) 1)))))))

(defthm case-1/4-2-a-9
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (+ 1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (+ 1 (ash (dgb->dgn (cdr dgop)) 1)))))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-9.0)
	        ))))

(defthm case-1/4-2-a-10
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop)))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (+ 1 (ash (dgb->dgn (cdr dgop)) 1)))))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-8)
	       (:instance case-1/4-2-a-9)
	       (:instance equal-equal 
			  (a (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)))
			  (b (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (+ 1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))))
			  (c (logxor (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 d)
				  (+ 1 (ash (dgb->dgn (cdr dgop)) 1))))))
	        ))))



(defthm case-1/4-2-a
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(logbitp d (dgb->dgn dgop))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-0 )
	       (:instance case-1/4-2-a-10)
	       (:instance case-1/4-2-a-2))
	       )))




;;;---------------------------------------------------

;;; Case 2.b.2 (logbitp (- d 1) (dgb->dgn dgop))


(defthm case-1/4-2-b-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash (ash -1 d) -1)
			     (ash (dgb->dgn dgop)  -1))
		     (logandc1 (ash (ash -1 d) -1)
			       (dgb->dgn dgop))))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (dgop (dgb->dgn dgop)))
	       ))))

(defthm case-1/4-2-b-2.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 (- d 1))
				  (ash (+ 1 (ash (dgb->dgn (cdr dgop)) 1)) -1))
		     (logandc1 (ash -1 (- d 1))
			       (+ 1 (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	  :use ((:instance case-1/4-2-b-1))
	       )))

(defthm case-1/4-2-b-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (+ 1 (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	  :use ((:instance case-1/4-2-a-2.0)
		(:instance ash-1-1-1 (n (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-2-b-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))
		)
	   (equal (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
		  (logxor (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1))
		     (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (d (- d 1))
			  (dgop (dgb->dgn (cdr dgop)))))
	       )))




(defthm case-1/4-2-b-4-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))
		)
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (ash (logxor (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1))
		     (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop)))) 1)
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-b-3)
	       ))))

(defthm natp-logand-ash-3
  (implies (and (natp d) 
		(> d 1)
		(not (= d 0))
		(natp n)
		)
	   (natp (logand (ash (ash -1 (- d 1)) -1)
			 n)))
:hints (("Goal" :in-theory (enable expt ash logand))))

(defthm natp-logand-ash-dgb->dgn-cdr-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (natp (logand (ash (ash -1 (- d 1)) -1)
			 (ash (dgb->dgn (cdr dgop)) -1))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance natp-logand-ash-3 (n (ash (dgb->dgn (cdr dgop)) -1)))))))


(defthm natp-logandc1-ash-3
  (implies (and (natp d) 
		(not (= d 0))
		(natp n)
		(> d 1)
		)
	   (natp (logandc1 (ash (ash -1 (- d 1)) -1)
			 n)))
:hints (("Goal" :in-theory (enable expt ash logand))))

(defthm natp-logandc1-ash-dgb->dgn-cdr-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (natp (logandc1 (ash (ash -1 (- d 1)) -1)
			 (dgb->dgn (cdr dgop)))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance natp-logandc1-ash-3 (n (dgb->dgn (cdr dgop))))))))



(defthm case-1/4-2-b-4-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logxor (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop)) -1))
		     (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop)))) 1)
		  (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance natp-logand-ash-dgb->dgn-cdr-4)
	       (:instance natp-logandc1-ash-dgb->dgn-cdr-4)
	       (:instance ash-logxor
			  (n1 (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)))
			  (n2 (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop)))))))))



(defthm case-1/4-2-b-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-2-b-4-1)
	       (:instance case-1/4-2-b-4-2)
	       (:instance equal-equal
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (ash (logxor (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1))
		     (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop)))) 1))
			  (c (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1))))
	        )
	       )))



(defthm case-1/4-2-b-5-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
		  (logand (ash (ash (ash -1 (- d 1)) -1) 1)
			  (ash (ash (dgb->dgn (cdr dgop))  -1) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logand-integer 
			  (n1 (ash (ash -1 (- d 1)) -1))
			  (n2 (ash (dgb->dgn (cdr dgop)) -1)))
	       )
	       )))


(defthm ash-ash--1-d-1
  (implies (and (natp d)
		(> d 1))
	   (equal (ash (ash (ash -1 (- d 1)) -1) 1)
		  (ash -1 (- d 1))))
  :hints (("Goal" :in-theory (enable ash))))

(defthm case-1/4-2-b-5-1-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
		  (logand (ash -1 (- d 1))
			  (dgb->dgn (cdr dgop)))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-2-b-5-1)
	       (:instance ash-ash--1-d-1)
	       (:instance logand-ash-ash-integer
			  (d (- d 1))
			  (n (dgb->dgn (cdr dgop)))))
	       )))


(defthm case-1/4-2-b-5-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1)
		  (logandc1 (ash (ash (ash -1 (- d 1)) -1) 1)
			       (ash (dgb->dgn (cdr dgop)) 1))

		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-logandc1-integer 
			  (n1 (ash (ash -1 (- d 1)) -1))
			  (n2 (dgb->dgn (cdr dgop))))
	       )
	       )))

(defthm case-1/4-2-b-5-2-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (equal (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1)
		  (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance ash-ash--1-d-1)
	       (:instance case-1/4-2-b-5-2)
	       )
	       )))


(defthm case-1/4-2-b-5-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		)
	   (equal (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-2-b-5-1-b)
	       (:instance case-1/4-2-b-5-2-b)
	       )
	       )))


(defthm case-1/4-2-b-5
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash 1dlop-dgop logxor logbitp 
			     dgb->dgn logandc1)
	 :use ((:instance case-1/4-2-b-4)
	       (:instance case-1/4-2-b-5-3)
	       (:instance equal-equal 
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (ash (logand (ash (ash -1 (- d 1)) -1)
			     (ash (dgb->dgn (cdr dgop))  -1)) 1)
			  (ash (logandc1 (ash (ash -1 (- d 1)) -1)
			       (dgb->dgn (cdr dgop))) 1)))
			  (c (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )))
	       )
	       )))


(defthm case-1/4-2-b-6.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ( (:instance logbitp-d>1=>logbitp-d-1)
	       (:instance case-1/4-2-b-5)
	       )
	       )))



(defthm not-logbitp-d>1=>not-logbitp-d-1-bis
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 1)
		(not (logbitp d (dgb->dgn dgop))))
	   (not (logbitp (- d 1) (dgb->dgn (cdr dgop)))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-my-logbitp-d=>not-my-lobitp-d-1)
	       (:instance my-logbitp-logbitp-b)
	       (:instance my-logbitp-logbitp-b (d (- d 1)) (dgop (cdr dgop))))))
)



(defthm case-1/4-2-b-6
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-logbitp-d>1=>not-logbitp-d-1-bis)
	       (:instance case-1/4-2-b-6.0)
	       )
	       )))


(defthm case-1/4-2-b-6.2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (+ 1 (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  ))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-b-6)
	       (:instance equal+1
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (logand (ash -1 (- d 1))
			 (dgb->dgn (cdr dgop)))
		     (logandc1 (ash -1 (- d 1))
			       (ash (dgb->dgn (cdr dgop)) 1))
		  )))
	       )
	       )))



(defthm case-1/4-2-b-7.1-d
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (evenp (logand (ash -1 (- d 1)) (dgb->dgn (cdr dgop)))))
	   
:hints (("Goal" :do-not-induct t
	 :in-theory (disable logandc1 logxor logand ash
			     dgb->dgn logbitp)
	 :use ((:instance natp-dgb->dgn-2)
	       (:instance logand-ash-evenp (d (- d 1))
			  (a (dgb->dgn (cdr dgop))))
	       ))))

(in-theory (disable LOGAND-ASH-ASH-INTEGER
		    ))

(defthm case-1/4-2-b-7.4-c
  (implies (and (natp d) 
		(natp a)
		(> d 1)
		(not (= d 0))
		)
	   (natp (logand (ash -1 (- d 1)) a))))

(defthm case-1/4-2-b-7.4-d
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (natp (logand (ash -1 (- d 1)) (dgb->dgn (cdr dgop)))))
  :hints (("Goal" :use ((:instance case-1/4-2-b-7.4-c
				   (a (dgb->dgn (cdr dgop))))))))
	   

(defthm case-1/4-2-b-7.2-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (evenp (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))))
	   
:hints (("Goal" :do-not-induct t
	 :in-theory (disable logandc1 logxor logand
			     dgb->dgn logbitp ash-to-floor)
	 :use ((:instance natp-dgb->dgn-2)
	       (:instance evenp-ash-n-1 (n (dgb->dgn (cdr dgop))))
	       (:instance logandc1-ash-evenp-b
			  (d (- d 1))
			  (a (dgb->dgn (cdr dgop))))
	       ))))


(defthm case-1/4-2-b-7.3-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (natp (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))))
	   )



(defthm case-1/4-2-b-7
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (+ 1 (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (1+ (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-b-7.1-d)
	       (:instance case-1/4-2-b-7.2-b)
	       (:instance case-1/4-2-b-7.3-b)
	       (:instance case-1/4-2-b-7.4-d)
	       (:instance logxor-1-evenp-evenp
			  (n1 (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop))))
			  (n2 (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1)))))
	       )))

(defthm case-1/4-2-b-8
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (1+ (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-b-7)
	       (:instance case-1/4-2-b-6.2)
	       (:instance equal-equal
			  (a (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)))
			  (b (+ 1 (logxor (logand (ash -1 (- d 1))
						  (dgb->dgn (cdr dgop)))
					  (logandc1 (ash -1 (- d 1))
						     (ash (dgb->dgn (cdr dgop)) 1))
					  )))
			  (c (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (1+ (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))))))
	       ))))



(defthm evenp-ash-1-d-1
  (implies (and (natp d)
		(> d 1))
	   (evenp (ash -1 (- d 1))))
  :hints (("Goal" :in-theory (enable ash evenp))))

(defthm case-1/4-2-b-9.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (+ 1 (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))) 
		  (logandc1 (ash -1 (- d 1))
				 (+ 1  (ash (dgb->dgn (cdr dgop)) 1))))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance evenp-ash-1-d-1)
	       (:instance natp-dgb->dgn-2)
	       (:instance evenp-ash-n-1 (n (dgb->dgn (cdr dgop))))
	       (:instance logandc1-1-evenp-evenp-b
			  (n1 (ash -1 (- d 1)))
			  (n2 (ash (dgb->dgn (cdr dgop)) 1)))))))

(defthm case-1/4-2-b-9
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (1+ (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1))))
		  (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 (- d 1))
				 (+ 1  (ash (dgb->dgn (cdr dgop)) 1)))))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-b-9.0)
	        ))))

(defthm case-1/4-2-b-10
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop)))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 (- d 1))
				 (+ 1  (ash (dgb->dgn (cdr dgop)) 1)))))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-b-8)
	       (:instance case-1/4-2-b-9)
	       (:instance equal-equal 
			  (a (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)))
			  (b (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (1+ (logandc1 (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) 1)))))
			  (c (logxor (logand (ash -1 (- d 1))
				  (dgb->dgn (cdr dgop)))
			  (logandc1 (ash -1 (- d 1))
				 (+ 1  (ash (dgb->dgn (cdr dgop)) 1))))))
	        ))))



(defthm case-1/4-2-b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(logbitp (- d 1) (dgb->dgn dgop))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-0 )
	       (:instance case-1/4-2-b-10)
	       (:instance case-1/4-2-b-2))
	       )))





;;; Case 2.c (not (logbitp d)) (not (logbitp (- d 1)))


(defthm case-1/4-2-c-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logandc1 (ash -1 d)
			       (dgb->dgn dgop))
			  (logand (ash -1 d)
			 (ash (dgb->dgn dgop) -1))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (dgop (dgb->dgn dgop)))
	       ))))

(defthm case-1/4-2-c-2.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logandc1 (ash -1 d)
			       (+ 1 (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (ash (+ 1 (ash (dgb->dgn (cdr dgop)) 1)) -1))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	  :use ((:instance case-1/4-2-a-1))
	       )))


(defthm case-1/4-2-c-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (1dlop-dgop d (dgb->dgn dgop))
		  (logxor (logandc1 (ash -1 d)
				    (+ 1 (ash (dgb->dgn (cdr dgop)) 1))
				    )
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-c-2.0)
		(:instance ash-1-1-1 (n (dgb->dgn (cdr dgop)))))
	       )))

(defthm natp-dgb->dgn-2
  (implies (dgb-p (cdr dgop))
	   (natp (dgb->dgn (cdr dgop)))))

(defthm integer-dgb->dgn
  (implies (dgb-p (cdr dgop))
	   (integerp (dgb->dgn (cdr dgop))))
:hints (("Goal" :use ((:instance  NATP-DGB->DGN-2)))))


(defthm case-1/4-2-c-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
		  (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			  (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
		     )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance 1dlop-dgop (d (- d 1))
			  (dgop (dgb->dgn (cdr dgop)))))
	       )))




(defthm case-1/4-2-c-4-1
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (ash (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			(logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))
			  ) 1)
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-c-3)
	       ))))


(defthm case-1/4-2-c-4-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			       (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))) 1)
		  (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
			  (ash (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1)) 1))
		  ))
:hints (("Goal" :do-not-induct t
	 :use (
	       (:instance natp-logand-ash-dgb->dgn-cdr-2)
	       (:instance natp-logandc1-ash-dgb->dgn-cdr-2)
	       (:instance ash-logxor
			  (n1 (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop))))
			  (n2 (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))))))))




(defthm case-1/4-2-c-4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  )
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop)
	 :use ((:instance case-1/4-2-c-4-1)
	       (:instance case-1/4-2-c-4-2)
	       (:instance equal-equal
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (ash (logxor (logandc1 (ash -1 (- d 1))
			       (dgb->dgn (cdr dgop)))
			       (logand (ash -1 (- d 1))
				  (ash (dgb->dgn (cdr dgop)) -1))) 1))
			  (c (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  )))
	        )

	        )
	       ))






(defthm case-1/4-2-c-5-3
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  )
		  (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash dgb->dgn)
	 :use ((:instance case-1/4-2-a-5-1-b)
	       (:instance case-1/4-2-a-5-2-b)
	       )
	       )))

(defthm case-1/4-2-c-5
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp (- d 1) (dgb->dgn (cdr dgop))))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))
		  ))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable ash 1dlop-dgop logxor logbitp 
			     dgb->dgn logandc1)
	 :use ((:instance case-1/4-2-c-4)
	       (:instance case-1/4-2-c-5-3)
	       (:instance equal-equal 
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (ash (logandc1 (ash -1 (- d 1))
					 (dgb->dgn (cdr dgop))) 1)
		   (ash (logand (ash -1 (- d 1))
				       (ash (dgb->dgn (cdr dgop)) -1)) 1)
			  ))
			  (c (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))))
	       )
	       )))


(defthm case-1/4-2-c-6.0
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-logbitp-d>1=>not-logbitp-d-1-bis)
	       (:instance case-1/4-2-c-5))
	       )))

(defthm not-logbitp-d-1=>not-logbitp-d-1-1-bis
  (implies (and (dgb-p dgop)
		(natp d)
		(> d 1)
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (not (logbitp (- (- d 1) 1) (dgb->dgn (cdr dgop)))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable logbitp dgb->dgn)
	 :use ((:instance not-my-logbitp-d-1=>not-my-lobitp-d-1-1)
	       (:instance not-my-logbitp-not-logbitp-b (d (- d 1)))
	       (:instance not-my-logbitp-not-logbitp-b (d (- (- d 1) 1)) (dgop (cdr dgop))))))
)



(defthm case-1/4-2-c-6
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)
		  (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-logbitp-d-1=>not-logbitp-d-1-1-bis)
	       (:instance case-1/4-2-c-6.0))
	       )))

(defthm case-1/4-2-c-6.2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (+ 1 (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  ))
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-c-6)
	       (:instance equal+1
			  (a (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
			  (b (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )))
	       )
	       )))

(defthm logxor-1-evenp-evenp-2
  (implies (and (natp n1)
		(natp n2)
		(evenp n1)
		(evenp n2))
	   (equal (+ 1 (logxor n1 n2))
		  (logxor (1+ n1) n2)))
:hints (("Goal" :use ((:instance logxor-1-evenp-evenp-aux)
			(:instance logxor-1-evenp-evenp-aux-4)))))



(defthm case-1/4-2-c-7
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		)
	   (equal (+ 1 (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
			(logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  ))
		  (logxor (1+ (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-7.1)
	       (:instance case-1/4-2-a-7.2)
	       (:instance case-1/4-2-a-7.3)
	       (:instance case-1/4-2-a-7.4)
	       (:instance logxor-1-evenp-evenp-2
			  (n2 (logand (ash -1 d)
				  (dgb->dgn (cdr dgop))))
			  (n1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))))
	       )))



(defthm case-1/4-2-c-8
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (logxor (1+ (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )
		  ))
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-c-7)
	       (:instance case-1/4-2-c-6.2)
	       (:instance equal-equal
			  (a (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)))
			  (b (+ 1 (logxor (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1))
					  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )))
			  (c (logxor (1+ (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )))
	       ))))




(defthm case-1/4-2-c-9
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (logxor (+ 1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )
		  (logxor (logandc1 (ash -1 d)
				  (+ 1 (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  ))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-a-9.0)
	        ))))

(defthm case-1/4-2-c-10
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(> d 1)
		(not (= d 0))
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop))))
	   (equal (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1))
		  (logxor (logandc1 (ash -1 d)
				  (+ 1 (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  ))
		  )
:hints (("Goal" :do-not-induct t
	 :use ((:instance case-1/4-2-c-8)
	       (:instance case-1/4-2-c-9)
	       (:instance equal-equal 
			  (a (+ 1 (ash (1dlop-dgop (- d 1) (dgb->dgn (cdr dgop))) 1)))
			  (b (logxor (+ 1 (logandc1 (ash -1 d)
				  (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  ))
			  (c (logxor (logandc1 (ash -1 d)
				  (+ 1 (ash (dgb->dgn (cdr dgop)) 1)))
			  (logand (ash -1 d)
				  (dgb->dgn (cdr dgop)))
			  )))
	        ))))


(defthm case-1/4-2-c
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(not (logbitp d (dgb->dgn dgop)))
		(not (logbitp (- d 1) (dgb->dgn dgop)))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-0 )
	       (:instance case-1/4-2-c-10)
	       (:instance case-1/4-2-c-2))
	       )))

(defthm case-1/4-2.b
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(= (car dgop) 1)
		(not (= d 0))
		(> d 1)
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-2-a)
	       (:instance case-1/4-2-b)
	       (:instance case-1/4-2-c)
	       )
	       )))


(defthm case-1/4-2
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (= d 0))
		(> d 1)
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-2.a)
	       (:instance case-1/4-2.b)
	       ))))



(defthm case-1/4
  (implies (and (natp d) 
		(dgb-p dgop)
		(not (endp dgop))
		(not (and (= d 1) (= (car dgop) 1)))
		(not (= d 0))
		(implies (and (natp (+ -1 d)) (dgb-p (cdr dgop)))
			 (equal (dgb->dgn (1dlop-dgop-binary (- d 1) (cdr dgop)))
				(1dlop-dgop (- d 1) (dgb->dgn (cdr dgop)))
				)))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable 1dlop-dgop-binary 1dlop-dgop dgb->dgn)
	 :use ((:instance case-1/4-1)
	       (:instance case-1/4-2)
	       ))))





(defthm 1dlop-dgop-1dlop-dgop-binary-aux
  (implies (and (natp d) (dgb-p dgop))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
  :hints (("Goal" :induct (1dlop-dgop-binary d dgop))
	  ("Subgoal *1/4'" :use ((:instance case-1/4)))
	  ("Subgoal *1/3'" :use ((:instance case-1/3)))
	  ("Subgoal *1/2'" :use ((:instance case-1/2))))
  )


;;;************************************************************
;;;
;;; Remove-final-zeros properties
;;;
;;;************************************************************


(defthm all-zeros-p-dgb->dgn-aux-1
  (implies (and (quasi-dgb-p dgop)	
		(all-zeros-p dgop))
	   (equal (dgb->dgn dgop)
		  0)))

(defthm all-zeros-p-dgb->dgn-aux-2
  (implies (and (quasi-dgb-p dgop)	
		(all-zeros-p dgop))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  0))
:hints (("Goal" :use ((:instance remove-initial-zeros-append-0/1-b)))))




(defthm all-zeros-p-dgb->dgn
  (implies (and (quasi-dgb-p dgop)
		(all-zeros-p dgop))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
:hints (("Goal" :use ((:instance all-zeros-p-dgb->dgn-aux-1)
		      (:instance all-zeros-p-dgb->dgn-aux-2)))))



(defthm dgb->dgn-rmove-final-zeros-aux-1/3-1
  (implies (and (quasi-dgb-p dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(all-zeros-p dgop))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
:hints (("Goal" :use ((:instance all-zeros-p-dgb->dgn)
		      ))))
	   

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0
  (implies (and (quasi-dgb-p dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 0))
	   (equal (dgb->dgn dgop)
		  (+ 0 (ash (dgb->dgn (cdr dgop)) 1))
		  )))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.1
  (implies (and (quasi-dgb-p dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 1))
	   (equal (dgb->dgn dgop)
		  (+ 1 (ash (dgb->dgn (cdr dgop)) 1))
		  )))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help
  (equal (dgb->dgn (append '(0) a))
	 (+ 0 (ash (dgb->dgn a) 1))
		  ))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p (cdr dgop)))
		(eql (car dgop) 0))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (dgb->dgn (append '(0) (remove-final-zeros (cdr dgop))))
		  )) 
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance
			 dgb->dgl-remove-final-zeros-help-1/3-aux3)
			))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 0))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (+ 0 (ash (dgb->dgn (remove-final-zeros (cdr dgop))) 1))
		  ))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help2)
			(:instance  dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1-help
				    (a (remove-final-zeros (cdr dgop))))))))

(defthm append-1-remove-final
  (implies (and (consp dgop)
		(eql (car dgop) 1)
		(quasi-dgb-p dgop)
		(not (all-zeros-p dgop)))
	   (equal (remove-final-zeros dgop)
		  (append '(1) (remove-final-zeros (cdr dgop))))))


(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help
  (equal (dgb->dgn (append '(1) a))
	 (+ 1 (ash (dgb->dgn a) 1))
		  ))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p (cdr dgop)))
		(eql (car dgop) 1))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (dgb->dgn (append '(1) (remove-final-zeros (cdr dgop))))
		  )) 
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance append-1-remove-final
			 )
			))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 1))
	   (equal (dgb->dgn (remove-final-zeros dgop))
		  (+ 1 (ash (dgb->dgn (remove-final-zeros (cdr dgop))) 1))
		  ))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help2)
			(:instance  dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2-help
				    (a (remove-final-zeros (cdr dgop))))))))



(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.a
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 0))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))
		  ))
:hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.1)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0
				    )))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2.b
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		(eql (car dgop) 1))
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))
		  ))
:hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0.2)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.0
				    )))))

(defthm dgb->dgn-rmove-final-zeros-aux-1/3-2
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		(not (all-zeros-p dgop))
		)
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))
		  ))
:hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.a)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2.b)))))


(defthm dgb->dgn-rmove-final-zeros-aux-1/3
  (implies (and (quasi-dgb-p dgop)
		(consp dgop)
		(equal (dgb->dgn (cdr dgop))
		  (dgb->dgn (remove-final-zeros (cdr dgop))))
		)
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))
		  ))
:hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance dgb->dgn-rmove-final-zeros-aux-1/3-1)
		 (:instance dgb->dgn-rmove-final-zeros-aux-1/3-2)))))

(defthm dgb->dgn-remove-final-zeros
  (implies (quasi-dgb-p dgop)
	   (equal (dgb->dgn dgop)
		  (dgb->dgn (remove-final-zeros dgop))))
  :hints (("Goal" :in-theory (disable remove-final-zeros)
	   :induct (dgb->dgn dgop))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defthm 1dlop-dgop-remove-final-zeros-1dlop-dgop-binary-aux
  (implies (and (natp d) (dgb-p dgop))
	   (equal (dgb->dgn (1dlop-dgop-binary d dgop))
		  (dgb->dgn (remove-final-zeros (1dlop-dgop-binary d dgop)))
		  ))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance quasi-dgb-p-1dlop-dgop-binary)
		 (:instance dgb->dgn-remove-final-zeros
			    (dgop (1dlop-dgop-binary d dgop)))
		 )) 
  ))

(defthm 1dlop-dgop-remove-final-zeros-1dlop-dgop-binary
  (implies (and (natp d) (dgb-p dgop))
	   (equal (dgb->dgn (remove-final-zeros (1dlop-dgop-binary d dgop)))
		  (1dlop-dgop d (dgb->dgn dgop))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance 1dlop-dgop-1dlop-dgop-binary-aux)
		 (:instance 1dlop-dgop-remove-final-zeros-1dlop-dgop-binary-aux)
		 (:instance equal-equal
			    (a (dgb->dgn (remove-final-zeros (1dlop-dgop-binary d dgop))))
			    (b (dgb->dgn (1dlop-dgop-binary d dgop)))
			    (c (1dlop-dgop d (dgb->dgn dgop))))))  
  ))


(defthm 1dlop-dgop-final-1dlop-dgop-binary
  (implies (and (natp d) (dgb-p dgop))
	   (equal (dgb->dgn (final-1dlop-dgop-binary d dgop))
		  (1dlop-dgop d (dgb->dgn dgop))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance final-1dlop-dgop-binary)
		 (:instance 1dlop-dgop-remove-final-zeros-1dlop-dgop-binary)
		 ))  
  ))


(defthm 1dlop-dgop-final-1dlop-dgop-binary-2
  (implies (and (natp d) (natp dgop))
	   (equal (dgb->dgn (final-1dlop-dgop-binary d (dgn->dgb dgop)))
		  (1dlop-dgop d dgop)))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable remove-final-zeros)
	   :use ((:instance 1dlop-dgop-final-1dlop-dgop-binary
			    (dgop (dgn->dgb dgop))
		 ))  
  )))



(defthm 1dlop-dgop-cmp-d-ls-induct
  (implies (and (natp d) (natp dgop))
	   (equal (1dlop-dgop d dgop)
		  (dgb->dgn (dgl->dgb (cmp-d-ls-induct d (dgb->dgl (dgn->dgb dgop)))))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable 1dlop-dgop  remove-final-zeros)
	   :use ((:instance 1dlop-dgop-final-1dlop-dgop-binary-2)
		 (:instance final-1dlop-dgop-binary-cmp-d-ls-induct
			    (dgop (dgn->dgb dgop))))  
  )))

(DEFTHM IMP-BINARY-IMP-EAT-INV-AUX-2
  (IMPLIES (DGB-P DGOP)
	   (DGL-P (DGB->DGL DGOP))))

(DEFTHM DGL-P-CMP-D-LS-INDUCT
  (IMPLIES (AND (NATP I) (DGL-P LS))
	   (DGL-P (CMP-D-LS-INDUCT I LS))))

(DEFTHM DGB-P-DGN->DGB
  (IMPLIES (NATP DGN)
	   (DGB-P (DGN->DGB DGN))))

(defthm 1dlop-dgop-cmp-d-ls-induct-2
  (implies (and (natp d) (natp dgop))
	   (equal (1dlop-dgop d dgop)
		  (dgop-ext-int (cmp-d-ls-induct d (dgop-int-ext dgop)))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable 1dlop-dgop  remove-final-zeros)
	   :use ((:instance 1dlop-dgop-cmp-d-ls-induct)
		 )  
  )))

(defthm 1dlop-dgop-cmp-d-ls-induct-3
  (implies (and (natp d) (natp dgop))
	   (equal (dgop-int-ext (1dlop-dgop d dgop))
		  (cmp-d-ls-induct d (dgop-int-ext dgop))))
  :hints (("Goal" :do-not-induct t
	   :in-theory (disable 1dlop-dgop  remove-final-zeros)
	   :use ((:instance 1dlop-dgop-cmp-d-ls-induct-2)
		 )  
  )))


(defthm natp-1dlop-dgop
  (implies (and (natp d)
		(natp dgop))
	   (natp (1dlop-dgop d dgop))))
